Various extensions#23
Conversation
maximebuyse
force-pushed
the
openmls-extensions
branch
from
6c72f41 to
3a448b9
Compare
abentkamp
left a comment
abentkamp
left a comment
There was a problem hiding this comment.
Lovely! I have a couple of comments: some missing tests, some opinons on Lean implementations of rust primitives, some questions...
| proptest! { | ||
| #[test] | ||
| fn test_clone(x in any::<u8>()) { | ||
| let model = x.inject(); | ||
| prop_assert_eq!(model.clone(), model); | ||
| } | ||
|
|
||
| #[test] | ||
| fn test_clone_bool(x in any::<bool>()) { | ||
| prop_assert_eq!(crate::clone::Clone::clone(x), x); | ||
| } |
There was a problem hiding this comment.
I'm guessing that inject is the identity on these types, but maybe we should be consistent?
Are there tests missing for all other integer types other than u8?
In one test, we use core's clone, in the other we use core model's clone. Shouldn't we use both in both tests?
| // Use the primitive length directly rather than `x.len()`: the latter | ||
| // extracts to a reference to `slice::Slice::len`, which (under | ||
| // `-core-models-lib`) Aeneas emits as an external-looking name with no | ||
| // dependency edge, producing a forward reference here (this `convert` | ||
| // module is extracted before `slice`). | ||
| if rust_primitives::slice::slice_length(x) == N { |
There was a problem hiding this comment.
This looks like Claude felt a bit too chatty :-).
Does this need a comment at all? If so, I would write: "Use rust primitive instead of x.len() to avoid forward reference in Lean."
| #[test] | ||
| fn test_as_ref_identity(x in any::<u8>()) { | ||
| prop_assert_eq!(super::AsRef::as_ref(x.inject()), x); | ||
| fn test_as_ref_slice_identity(v in prop::collection::vec(any::<u8>(), 0..=8)) { | ||
| let s: &[u8] = &v[..]; | ||
| prop_assert_eq!(super::AsRef::as_ref(s), s); | ||
| } |
There was a problem hiding this comment.
Wasn't a test for u8 good to have as well? Maybe too trivial?
Should we call inject? and apply as_ref on both sides?
| macro_rules! impl_hash_for_int { | ||
| ($($t:ty),*) => { | ||
| $( | ||
| #[hax_lib::attributes] | ||
| impl Hash for $t { | ||
| fn hash<H: Hasher>(&self, mut h: H) -> H { | ||
| h.write(&[*self as u8]); | ||
| h | ||
| } | ||
| } | ||
| )* | ||
| }; |
There was a problem hiding this comment.
Can't we implement this correctly? Should we establish some way of keeping track where we intentionally deviate from the official implementation?
| #[hax_lib::attributes] | ||
| #[cfg_attr(charon, aeneas::exclude)] | ||
| //#[cfg_attr(charon, aeneas::exclude)] | ||
| impl<T> Slice<T> { |
There was a problem hiding this comment.
Remove instead of commenting out?
| ); | ||
| } | ||
|
|
||
| // ----- get_unchecked (in-bounds) ------------------------------------- |
There was a problem hiding this comment.
Lots of tests missing here for the different Range* variants.
| ok (sub, fun ss => match Slice.update_subslice s ⟨b, e⟩ ss with | ||
| | .ok r => r | ||
| | _ => s) |
There was a problem hiding this comment.
I think using ⟨ s.val.setSlice! ..., by scalar_tac ⟩ might be more elegant here: Matching on a Result value inside the Result monad is a bit odd. But we would then have to check whether ss has the correct length.
I also suspect that what's implemented here is not the correct behavior for the case where ss has not the correct length? Or is this impossible to do in Rust?
| @[rust_fun "rust_primitives::slice::slice_reverse"] | ||
| def rust_primitives.slice.slice_reverse | ||
| {T : Type} : Slice T → Result (Slice T) := | ||
| fun s => ok ⟨ s.val.reverse, by have := s.property; simp [*] ⟩ |
There was a problem hiding this comment.
I'm guessing by simp [s.property] would do as well?
| // ============================================================================= | ||
| // div_ceil (unsigned) | ||
| // ============================================================================= |
| // ----- get_unchecked (in-bounds) --------------------------------------------- | ||
| // In-bounds is the only defined behaviour; the model projects like `index`. | ||
|
|
There was a problem hiding this comment.
What about get_mut and get_unchecked_mut? What about all the Range* variants?
2 participants
No description provided.